es:ES, C, T:Type, S1, S2:(CCE), codes1:(j,i:Ce:{x:E| S1(j,i,x)} state@loc(e)T),
codes2:(j,i:Ce:{x:E| S2(j,i,x)} state@loc(e)T), dec_S1:(j,i:Ce:EDec(S1(j,i,e))).
(j, i:C, e:E. (S1(j,i,e) & S2(j,i,e)))
 (j, i:C, e:{x:E| (S1(j,i,x))  (S2(j,i,x))} , st:state@loc(e).
 ((S1(j,i,e))  ([S1? codes1 : codes2](j,i,e,st) = codes1(j,i,e,st)))
 & ((S2(j,i,e))  ([S1? codes1 : codes2](j,i,e,st) = codes2(j,i,e,st)))) 

latex

Definitions	P  Q, s = t, <a, b>, [S? codes1 : codes2], P  Q, left + right, A, P & Q, x:A  B(x), Dec(P), {x:A| B(x)} , f(a), state@i, loc(e), x:AB(x), E, x:A. B(x), , Type, t  T, ES, if p:P then A(p) else B fi , False
Lemmas	event system wf, es-E wf, es-loc wf, es-state wf, decidable wf, not wf